A,B:es_realizer{i:l}.
R-interface(A; B)
 (i:Id. 
 (R-has-loc(B; i))
  fpf-all(Knd;
  fpf-all(Kind-deq;
  fpf-all(R-da(B; i);
  fpf-all(k,T.((isrcv(k))
  fpf-all( (destination(lnk(k)) = i  Id)
  fpf-all( subtype_rel(fpf-cap(R-da(A; source(lnk(k))); Kind-deq; k; void); T)))) 

latex

Definitions	True, b, top, Knd, ff, tt, if b then t else f fi , fpf-cap(f; eq; x; z), guard(T), sq_type(T), x. t(x), prop{i:l}, t  T, P  Q, P  Q, fpf-all(A; eq; f; x,v.P(x;v)), P  Q, R-interface(A; B), P  Q, x:A. B(x), Y, reduce(f; k; as), t.1, deq-member(eq; x; L), fpf-empty, P  Q, decidable(P), fpf-dom(eq; x; f), False, A, Unit, , x(s),
Lemmas	not-R-has-loc-R-da, decidable assert, assert of bnot, eqff to assert, not wf, bnot wf, iff transitivity, eqtt to assert, bool wf, Knd sq, isrcv-implies, Id sq, tagof wf, es realizer wf, fpf-ap wf, rcv wf, lsrc wf, fpf-cap wf, IdLnk wf, R-has-loc wf, top wf, fpf wf, fpf-trivial-subtype-top, R-da wf, Kind-deq wf, Knd wf, fpf-dom wf, isrcv wf, assert wf, lnk wf, ldst wf, Id wf